Nuprl Definition : w-first 0,22

first(e)
== if time(e)=0 true ; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>) else false fi
(recursive) 
latex



clarification:

w-first(we)
== if w-time(we)=0 true
== i; w-isnull(w; w-a(w; w-loc(we); (w-time(we)-1))) w-first(w; <w-loc(we),w-time(we)-1>)
== else false fi
(recursive) 
latex


DefinitionsY, x.A(x), i=j, true, if b t else f fi, isnull(a), a(i;t), f(a), <a,b>, loc(e), n-m, time(e), #$n, false
FDL editor aliasesw-first

origin